Nuprl Lemma : snd-it_wf
11,40
postcript
pdf
es
:ES,
ff
:FIFO,
p
:(E
),
e
:E,
sndr
,
rcvr
:
ff
.C. [
e
:
sndr
p
rcvr
]
latex
Definitions
x
:
A
.
B
(
x
)
,
,
t
T
,
[
e
:
i
p
j
]
,
P
&
Q
Lemmas
fifoS
wf
,
fifoC
wf
,
es-E
wf
,
FIFO
wf
,
event
system
wf
origin
es:ES, ff:FIFO, p:(E
), e:E, sndr, rcvr:ff.C. [e: sndr p rcvr] 
es:ES, ff:FIFO, p:(E), e:E, sndr, rcvr:ff.C. [e: sndr p rcvr] x:A. B(x) Tp j]